es:ES, a:Atom1, e:E.
loc(e) || a
 (e':E. (e' < e)  e' sends to loc(e) || a )
 es_state_when(es;es-init(es;e)):es_state(es;loc(e))||a
 e sends || a 

latex

Definitions

t  T, True, b, Void, x:AB(x), P  Q, False, A, x:A. B(x), x:A  B(x), ES, Atom$n, x:T||a, e sends || a, t.1, E, i || a, e@i. P(e), e sends to i || a , let x,y = A in B(x;y), P & Q, <a, b>, Id, s = t, e loc e' , isrcv(e), P  Q, P  Q, T, es_state(es;i), es_state_when(es;e), e receives || a, ee'.P(e), loc(e), Type, (e <loc e'), if b then t else f fi , e < e', (e < e'), sender(e), s ~ t, {T}, SQType(T), es-init(es;e), WellFnd{i}(A;x,y.R(x;y)), A c B, left + right, P  Q, x. t(x), first(e), , case b of inl(x) => s(x) | inr(y) => t(y), es_vartype(es;i;x), {x:A| B(x)}

Lemmas

squash wf, true wf, Id wf, es-loc wf, not wf, assert wf, es-first wf, es-locl-wellfnd, es-le-iff, es-init-elim2, es-pred-locl, es-init-elim, es-sender-causl, es-causl transitivity2, es-causle weakening locl, es-atom-lemma1, free-from-atom wf1, es state when wf, es state wf, es-isrcv-loc, es-le-loc, es-loc-init, es-loc-pred